>>> import z3
>>> a = z3.Int("a")
>>> b = z3.Bool("b")
>>> a + b
a + If(b, 1, 0)
>>> b + a
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1575, in __add__
    return If(self, 1, 0) + If(other, 1, 0)
                            ^^^^^^^^^^^^^^^
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1415, in If
    a = s.cast(a)
        ^^^^^^^^^
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1555, in cast
    _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 107, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value

>>> import z3
>>> b = z3.Bool("b")
>>> 1 + b
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: unsupported operand type(s) for +: 'int' and 'BoolRef'
>>> b + 1
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1575, in __add__
    return If(self, 1, 0) + If(other, 1, 0)
                            ^^^^^^^^^^^^^^^
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1415, in If
    a = s.cast(a)
        ^^^^^^^^^
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 1553, in cast
    _z3_assert(is_expr(val), msg % (val, type(val)))
  File "/tmp/z3-test/venv/lib/python3.11/site-packages/z3/z3.py", line 107, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: True, False or Z3 Boolean expression expected. Received 1 of type <class 'int'>